% !TEX root =  main.tex

%------------------------------------------------------------------------
% General TeX and LaTeX macros
%------------------------------------------------------------------------
\newcommand{\Fix}[1]{\textbf{[[}{\color{red} #1}\textbf{]]}}
\newcommand{\Todo}[1]{\footnote{\textbf{[[}{\color{blue}\textbf{TODO} #1}\textbf{]]}}}
\newcommand{\CodeIn}[1]{\begin{small}\texttt{#1}\end{small}}
\newcommand{\MathIn}[1]{\CodeIn{#1}}
\newcommand{\BoxIn}[1]{\begin{footnotesize}\texttt{#1}\end{footnotesize}}
\newcommand{\Email}[1]{{\normalsize\textit{#1}}}
\newcommand{\etal}{\emph{et al.\/}}
\newcommand{\ffont}[1]{\texttt{#1}}
\newcommand{\Ignore}[1]{}

%------------------------------------------------------------------------
% Tools
%------------------------------------------------------------------------
\newcommand{\tname}{STEP}
\newcommand{\ssa}{SSA}
\newcommand{\se}{SE}
\newcommand{\dsc}{{\textsc{}DSC}\xspace}
\newcommand{\spf}{{\textsc{}SPF}\xspace}
\newcommand{\JCute}{{\textsc{}JCute}\xspace}
\newcommand{\DSC}{{\textsc{}DSC}\xspace}
\newcommand{\SPF}{{\textsc{}SPF}\xspace}
\newcommand{\RUGRAT}{{\textsc{}RUGRAT}\xspace}

%------------------------------------------------------------------------
% KeY
%------------------------------------------------------------------------
\newcommand{\KeY}{Ke\kern-0.1emY}
\newcommand{\KeYFOL}{Ke\kern-0.1emY's logic}

%------------------------------------------------------------------------
% Java
%------------------------------------------------------------------------
\newcommand{\java}[1]{\texttt{\frenchspacing#1}}

%------------------------------------------------------------------------
% Alloy
%------------------------------------------------------------------------
\newcommand{\alloy}[1]{\texttt{\frenchspacing#1}}
\newcommand{\arity}[1]{\ensuremath{\mathit{arity}(\alloy{#1})}}

%------------------------------------------------------------------------
% Dynamic Logic
%------------------------------------------------------------------------
\newcommand{\dl}[1]{\texttt{\frenchspacing#1}}

%------------------------------------------------------------------------
% JML
%------------------------------------------------------------------------
\newcommand{\jml}[1]{\texttt{\frenchspacing#1}}
\newcommand{\jmlOld}[0]{\jml{\textbackslash old}}
\newcommand{\jmlResult}[0]{\jml{\textbackslash result}}
\newcommand{\jmlFresh}[0]{\jml{\textbackslash fresh}}
\newcommand{\jmlReach}[0]{\jml{\textbackslash reach}}
\newcommand{\jmlForall}[0]{\jml{\textbackslash forall}}
\newcommand{\jmlExists}[0]{\jml{\textbackslash exists}}
\newcommand{\jmlSum}[0]{\jml{\textbackslash sum}}
\newcommand{\jmlNumOf}[0]{\jml{\textbackslash num\_of}}
\newcommand{\jmlComment}[1]{\java{//@ #1}} %//$

%------------------------------------------------------------------------
% SMT-LIB
%------------------------------------------------------------------------
\newcommand{\smt}[1]{\textbf{#1}}
\newcommand{\smtlib}{SMT-LIB}

%------------------------------------------------------------------------
% Symbolic Execution
%------------------------------------------------------------------------
\newcommand{\Baseline}{\emph{Baseline}}
\newcommand{\CachingOpt}{\emph{CachingOpt}}
\newcommand{\Caching}{\emph{Caching}}
\newcommand{\Stackssa}{\emph{StackOpt}}
\newcommand{\Stacknonssa}{\emph{Stack}}
\newcommand{\baseline}{\emph{baseline}}
\newcommand{\cachingOpt}{\emph{cachingOpt}}
\newcommand{\caching}{\emph{caching}}
\newcommand{\stackssa}{\emph{stackOpt}}
\newcommand{\stacknonssa}{\emph{stack}}

%------------------------------------------------------------------------
% Mathematic
%------------------------------------------------------------------------
\newcommand{\arrow}[1]{$\overrightarrow{#1}$}
\newcommand{\lt}{$<$}
\newcommand{\gt}{$>$}
\newcommand{\zero}{\mathit{0}}
\newcommand{\one}{\mathit{1}}
\newcommand{\xa}{$\overrightarrow{x}$}

%------------------------------------------------------------------------
% Color
%------------------------------------------------------------------------
\newcommand{\changedbg}{\rowcolor[rgb]{0.8,0.8,0.8}}
\newcommand{\refactoredbg}{\rowcolor[rgb]{0.8,0.8,0.8}}
\newcommand{\bugbg}{\rowcolor[rgb]{0.8,0.8,0.8}}
\newcommand{\greycolor}{\rowcolor[rgb]{0.8,0.8,0.8}}
\newcommand{\tianhai}[1]{\textbf{[[tianhai: }{\color{blue} #1}\textbf{]]}}
\newcommand{\tianhaidel}[1]{{\color{blue} \sout{#1}}}
\newcommand{\tianhaiadd}[1]{\textbf{[[tianhai added: }{\color{blue} #1}\textbf{]]}}
%\newcommand{\tianhai}[1]{#1}